Inference at * 2 2 2 1 1 
Iof proof for Lemma member nth tl:



1. T : Type
2. n : 
3. 0 < n
4. x:T, L:(T List). (x  nth_tl(n - 1;L))  (x  L)
5. x : T
6. T List
7. u : T
8. v : T List
9. (x  nth_tl(n;v))  (x  v)
10. 0 < n
11. (x  nth_tl(n - 1;v))
  (x = u)  (x  v) 

latex

 by ((OrRight) 
CollapseTHEN (MaAuto)) 

latex

C.

Definitions	P  Q, {T}, nth_tl(n;as), n - m, #$n, x:A. B(x), x:A  B(x), (x  l), P  Q, type List, x:A. B(x), x:AB(x), a < b, , Type, t  T, , s = t
Lemmas	l member wf